FDL - Nuprl Lemma : decidable__rel

Nuprl Lemma : decidable__rel_plus-causl

x, y:E. (R(x,y))

x, y:E. Dec(R(x,y)))

y, x:E. Dec(R^+(x,y)))

Definitions	A, {T}, A c B, P Q, P Q, x. t(x), P & Q, x:A. B(x), x f y, P Q, t T, R^+, Dec(P), P Q, , x:A. B(x), False, WellFnd{i}(A;x,y.R(x;y)), x(s), S T
Lemmas	decidable es-E-equal, rel-star-iff-rel-plus-or, rel star wf, rel plus iff, es-causl-wellfnd, nat plus inc, rel exp wf, nat plus wf, decidable cand, decidable existse-causl, not wf, rel-rel-plus, rel plus wf, event system wf, es-causl wf, es-E wf, decidable wf